XM == P:. Dec(P) 

latex

---

clarification:

XM{i} == P:{i}. Dec(P) 

latex

Up	core 2, core 2
Wellformedness Lemmas	xmiddle wf, xmiddle wf
Definitions	x:A. B(x), , Dec(P)
FDL editor aliases	xmiddle